In this thesis we address problems related to the verification of software-based systems. We are mostly interested in the (safe) design of decision procedures used in verification. In addition, we also consider a modularity problem for a modeling language used in the Why verification platform. Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In order to build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting. This approach uses a general calculus for equational reasoning named paramodulation. In general, a fair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decision procedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge on satisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thus it becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulation calculus (SPC) has been studied, notably to automatically prove decidability of single theories and of their combinations. The advantage of SPC is that if it halts for one given abstract input, then PC halts for all the corresponding concrete inputs. More generally, SPC is an automated tool to check properties of PC like termination, stable infiniteness and deduction completeness. A major contribution of this thesis is a prototyping environment for designing and verifying decision procedures. This environment, based on the theoretical studies, is the first implementation of the schematic paramodulation calculus. It has been implemented from scratch on the firm basis provided by the Maude system based on rewriting logic. We show that this prototype is very useful to derive decidability and combinability of theories of practical interest in verification. It helps testing new saturation strategies and experimenting new extensions of the original (schematic) paramodulation calculus. This environment has been applied for the design of a schematic paramodulation calculus dedicated to the theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulation to a built-in theory. This study has led to new automatic proof techniques that are different from those performed manually in the literature. The assumptions to apply our proof techniques are easy to satisfy for equational theories with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures such as lists and records. We have also addressed the problem of modular specification of generic Java classes and methods. We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for proving that a Java or C program is a correct implementation of some specification. The key features are the introduction of parametricity both for types and for theories and an instantiation relation between theories. The proposed extensions are illustrated on two significant examples: the specification of the generic method for sorting arrays and for generic hash map. Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures are at the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a source program annotated by specifications, and then transmits them to SMT solvers or proof assistants to check the program correctness.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001094 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001094 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:tel-00910929
   |texte=   Schematic calculi for the analysis of decision procedures
}}